package tr.edu.ege.kipler.satisfiability.completion.rules.formula;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.CompletionRule;
import tr.edu.ege.kipler.satisfiability.container.WcsData;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldAccess;
import tr.edu.ege.kipler.syntax.KModality;
import tr.edu.ege.kipler.syntax.ModalExpression;
import tr.edu.ege.kipler.syntax.TypedModality;
import tr.edu.ege.kipler.syntax.WorldElement;

/**
 * This method handles a modal formula in which the modal operator is the
 * possibility operator having the axioms of the standard modal logic K.
 * 
 * @author İnanç Seylan
 * 
 */
public class DiamondFormulaRule extends CompletionRule {
	/**
	 * Since we have many modal operators (therefore necessity and possibility
	 * operators), this rule selects possibilitations according to the type of
	 * the possibility operator (belief, intention, etc.) we want. This field
	 * indicates the possibility operator.
	 */
	private TypedModality operator;

	private boolean applied;

	/**
	 * Default constructor that initializes the {@link #operator} field.
	 * 
	 * @param operator
	 *            The operator
	 */
	public DiamondFormulaRule(TypedModality operator) {
		this.operator = operator;
	}

	@Override
	public boolean isApplied() {
		return applied;
	}

	/**
	 * For all possibilitations with the specified modal operator, check if
	 * there is a world accessible that the possibilitate is true. If not, then
	 * create an accessible world from this world, and add the possibilitate to
	 * that world.
	 * 
	 * @see tr.edu.ege.seagent.alcbi.satisfiability.frame.CompletionRule#apply()
	 */
	public void apply() throws UnsatisfiableException {
		applied = false;
		for (WorldElement f : getWorld().getPBox().getFormulas()) {
			if (f instanceof ModalExpression) {
				ModalExpression mf = (ModalExpression) f;
				if (!mf.getOperator().isNecessiate()
						&& mf.getOperator() instanceof TypedModality
						&& mf.getOperator() instanceof KModality) {
					TypedModality modality = (TypedModality) mf.getOperator();
					if (modality.getType().equals(operator.getType())
							&& !suchAWorldExists(mf)) {
						createAndConnectWorld(mf);
					}
				}
			}
		}
	}

	/**
	 * Checks if there is an accessible world containing the possibilitate of
	 * the given formula.
	 * 
	 * @param mf
	 *            The possibilitation whose possibilitate that we'll search in
	 *            accessible world.
	 * @return true if such an accessible world exists.
	 */
	protected boolean suchAWorldExists(ModalExpression mf) {
		boolean conditionAlreadySatisfied = false;
		String relation = ((KModality) mf.getOperator()).getRelation();
		WorldElement f = mf.getExpression();
		for (World world : getWcs().getAccWorldsByFrom(relation, getWorld())) {
			if (world.contains(f)) {
				conditionAlreadySatisfied = true;
				break;
			}
		}
		return conditionAlreadySatisfied;
	}

	/**
	 * Creates a new world and adds the possibilitate of the modal formula given
	 * to that world.
	 * 
	 * @param mf
	 *            The possibilitation
	 * @return the world that has been created.
	 */
	protected World createAndConnectWorld(ModalExpression mf)
			throws UnsatisfiableException {
		WcsData wcsData = getWcs().getData();
		String relation = ((KModality) mf.getOperator()).getRelation();
		WorldElement newFormula = mf.getExpression();
		World world = getWcs().createWorld();
		// TODO: manage dependency
		getWcs().addConstraint(new WorldAccess(getWorld(), world, relation));
		wcsData.getLogger().info(
				"WCS " + getWcs().getId() + " Diamond Formula Rule: Adding "
						+ newFormula + " to the newly generated world "
						+ world.getName());// TODO: accessibility as a formula
		world.add(newFormula);
		applied = true;
		return world;
	}

}
